\begin{tabbing}
@${\it loc}$ \=precondition for $a$(v:$T$):\+
\\[0ex]$P$ State(${\it ds}$) v
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inr(inr(inr(inr(inr(inr(inl($\langle$${\it loc}$$,\,$${\it ds}$$,\,$$a$$,\,$$T$$,\,$$P$$\rangle$))))))))
\end{tabbing}